\begin{tabbing}
$M_{1}$ $\oplus$ $M_{2}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=mk{-}ma(fpf{-}join(IdDeq;1of($M_{1}$);1of($M_{2}$));\+
\\[0ex]fpf{-}join(KindDeq;1of(2of($M_{1}$));1of(2of($M_{2}$)));
\\[0ex]fpf{-}join(IdDeq;1of(2of(2of($M_{1}$)));1of(2of(2of($M_{2}$))));
\\[0ex]fpf{-}join(IdDeq;1of(2of(2of(2of($M_{1}$))));1of(2of(2of(2of($M_{2}$)))));
\\[0ex]fpf{-}join(product{-}deq(Knd;Id;KindDeq;IdDeq);1of(\=2of(2of(2of(2of(\+
\\[0ex]$M_{1}$)))));1of(2of(2of(2of(2of($M_{2}$))))));
\-\\[0ex]fpf{-}join(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);1of(\=2of(2of(2of(2of(2of(\+
\\[0ex]$M_{1}$))))));1of(\=2of(2of(2of(2of(\+
\\[0ex]2of($M_{2}$)))))));
\-\-\\[0ex]fpf{-}join(IdDeq;1of(2of(2of(2of(2of(2of(2of($M_{1}$)))))));1of(\=2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{2}$))))))));
\-\\[0ex]fpf{-}join(product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(\=2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{1}$))))))));1of(\=2of(2of(2of(2of(2of(\+
\\[0ex]2of(2of($M_{2}$)))))))));
\-\-\\[0ex]fpf{-}join(KindDeq;1of(\=2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{1}$)))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of($M_{2}$))))))))));
\-\\[0ex]fpf{-}join(KindDeq;1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{1}$))))))))));1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{2}$)))))))))));
\-\-\\[0ex]fpf{-}join(IdDeq;1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{1}$)))))))))));1of(\=2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(\+
\\[0ex]$M_{2}$)))))))))))))
\-\-\-
\end{tabbing}